0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 88 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 44 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 8 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
sublistC_in_gg([], T15) → sublistC_out_gg([], T15)
sublistC_in_gg(T5, .(T28, T29)) → U3_gg(T5, T28, T29, appendA_in_aag(X56, X57, T29))
appendA_in_aag([], T44, T44) → appendA_out_aag([], T44, T44)
appendA_in_aag(.(T49, X93), X94, .(T49, T50)) → U1_aag(T49, X93, X94, T50, appendA_in_aag(X93, X94, T50))
U1_aag(T49, X93, X94, T50, appendA_out_aag(X93, X94, T50)) → appendA_out_aag(.(T49, X93), X94, .(T49, T50))
U3_gg(T5, T28, T29, appendA_out_aag(X56, X57, T29)) → sublistC_out_gg(T5, .(T28, T29))
sublistC_in_gg(.(T71, T72), .(T71, T29)) → U4_gg(T71, T72, T29, appendA_in_gag(T72, T38, T29))
appendA_in_gag([], T44, T44) → appendA_out_gag([], T44, T44)
appendA_in_gag(.(T49, X93), X94, .(T49, T50)) → U1_gag(T49, X93, X94, T50, appendA_in_gag(X93, X94, T50))
U1_gag(T49, X93, X94, T50, appendA_out_gag(X93, X94, T50)) → appendA_out_gag(.(T49, X93), X94, .(T49, T50))
U4_gg(T71, T72, T29, appendA_out_gag(T72, T38, T29)) → sublistC_out_gg(.(T71, T72), .(T71, T29))
sublistC_in_gg(T81, .(T82, T29)) → U5_gg(T81, T82, T29, appendA_in_aag(T83, T38, T29))
U5_gg(T81, T82, T29, appendA_out_aag(T83, T38, T29)) → U6_gg(T81, T82, T29, appendB_in_agg(X123, T81, T83))
appendB_in_agg([], T90, T90) → appendB_out_agg([], T90, T90)
appendB_in_agg(.(T98, X148), T97, .(T98, T99)) → U2_agg(T98, X148, T97, T99, appendB_in_agg(X148, T97, T99))
U2_agg(T98, X148, T97, T99, appendB_out_agg(X148, T97, T99)) → appendB_out_agg(.(T98, X148), T97, .(T98, T99))
U6_gg(T81, T82, T29, appendB_out_agg(X123, T81, T83)) → sublistC_out_gg(T81, .(T82, T29))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
sublistC_in_gg([], T15) → sublistC_out_gg([], T15)
sublistC_in_gg(T5, .(T28, T29)) → U3_gg(T5, T28, T29, appendA_in_aag(X56, X57, T29))
appendA_in_aag([], T44, T44) → appendA_out_aag([], T44, T44)
appendA_in_aag(.(T49, X93), X94, .(T49, T50)) → U1_aag(T49, X93, X94, T50, appendA_in_aag(X93, X94, T50))
U1_aag(T49, X93, X94, T50, appendA_out_aag(X93, X94, T50)) → appendA_out_aag(.(T49, X93), X94, .(T49, T50))
U3_gg(T5, T28, T29, appendA_out_aag(X56, X57, T29)) → sublistC_out_gg(T5, .(T28, T29))
sublistC_in_gg(.(T71, T72), .(T71, T29)) → U4_gg(T71, T72, T29, appendA_in_gag(T72, T38, T29))
appendA_in_gag([], T44, T44) → appendA_out_gag([], T44, T44)
appendA_in_gag(.(T49, X93), X94, .(T49, T50)) → U1_gag(T49, X93, X94, T50, appendA_in_gag(X93, X94, T50))
U1_gag(T49, X93, X94, T50, appendA_out_gag(X93, X94, T50)) → appendA_out_gag(.(T49, X93), X94, .(T49, T50))
U4_gg(T71, T72, T29, appendA_out_gag(T72, T38, T29)) → sublistC_out_gg(.(T71, T72), .(T71, T29))
sublistC_in_gg(T81, .(T82, T29)) → U5_gg(T81, T82, T29, appendA_in_aag(T83, T38, T29))
U5_gg(T81, T82, T29, appendA_out_aag(T83, T38, T29)) → U6_gg(T81, T82, T29, appendB_in_agg(X123, T81, T83))
appendB_in_agg([], T90, T90) → appendB_out_agg([], T90, T90)
appendB_in_agg(.(T98, X148), T97, .(T98, T99)) → U2_agg(T98, X148, T97, T99, appendB_in_agg(X148, T97, T99))
U2_agg(T98, X148, T97, T99, appendB_out_agg(X148, T97, T99)) → appendB_out_agg(.(T98, X148), T97, .(T98, T99))
U6_gg(T81, T82, T29, appendB_out_agg(X123, T81, T83)) → sublistC_out_gg(T81, .(T82, T29))
SUBLISTC_IN_GG(T5, .(T28, T29)) → U3_GG(T5, T28, T29, appendA_in_aag(X56, X57, T29))
SUBLISTC_IN_GG(T5, .(T28, T29)) → APPENDA_IN_AAG(X56, X57, T29)
APPENDA_IN_AAG(.(T49, X93), X94, .(T49, T50)) → U1_AAG(T49, X93, X94, T50, appendA_in_aag(X93, X94, T50))
APPENDA_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPENDA_IN_AAG(X93, X94, T50)
SUBLISTC_IN_GG(.(T71, T72), .(T71, T29)) → U4_GG(T71, T72, T29, appendA_in_gag(T72, T38, T29))
SUBLISTC_IN_GG(.(T71, T72), .(T71, T29)) → APPENDA_IN_GAG(T72, T38, T29)
APPENDA_IN_GAG(.(T49, X93), X94, .(T49, T50)) → U1_GAG(T49, X93, X94, T50, appendA_in_gag(X93, X94, T50))
APPENDA_IN_GAG(.(T49, X93), X94, .(T49, T50)) → APPENDA_IN_GAG(X93, X94, T50)
SUBLISTC_IN_GG(T81, .(T82, T29)) → U5_GG(T81, T82, T29, appendA_in_aag(T83, T38, T29))
U5_GG(T81, T82, T29, appendA_out_aag(T83, T38, T29)) → U6_GG(T81, T82, T29, appendB_in_agg(X123, T81, T83))
U5_GG(T81, T82, T29, appendA_out_aag(T83, T38, T29)) → APPENDB_IN_AGG(X123, T81, T83)
APPENDB_IN_AGG(.(T98, X148), T97, .(T98, T99)) → U2_AGG(T98, X148, T97, T99, appendB_in_agg(X148, T97, T99))
APPENDB_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPENDB_IN_AGG(X148, T97, T99)
sublistC_in_gg([], T15) → sublistC_out_gg([], T15)
sublistC_in_gg(T5, .(T28, T29)) → U3_gg(T5, T28, T29, appendA_in_aag(X56, X57, T29))
appendA_in_aag([], T44, T44) → appendA_out_aag([], T44, T44)
appendA_in_aag(.(T49, X93), X94, .(T49, T50)) → U1_aag(T49, X93, X94, T50, appendA_in_aag(X93, X94, T50))
U1_aag(T49, X93, X94, T50, appendA_out_aag(X93, X94, T50)) → appendA_out_aag(.(T49, X93), X94, .(T49, T50))
U3_gg(T5, T28, T29, appendA_out_aag(X56, X57, T29)) → sublistC_out_gg(T5, .(T28, T29))
sublistC_in_gg(.(T71, T72), .(T71, T29)) → U4_gg(T71, T72, T29, appendA_in_gag(T72, T38, T29))
appendA_in_gag([], T44, T44) → appendA_out_gag([], T44, T44)
appendA_in_gag(.(T49, X93), X94, .(T49, T50)) → U1_gag(T49, X93, X94, T50, appendA_in_gag(X93, X94, T50))
U1_gag(T49, X93, X94, T50, appendA_out_gag(X93, X94, T50)) → appendA_out_gag(.(T49, X93), X94, .(T49, T50))
U4_gg(T71, T72, T29, appendA_out_gag(T72, T38, T29)) → sublistC_out_gg(.(T71, T72), .(T71, T29))
sublistC_in_gg(T81, .(T82, T29)) → U5_gg(T81, T82, T29, appendA_in_aag(T83, T38, T29))
U5_gg(T81, T82, T29, appendA_out_aag(T83, T38, T29)) → U6_gg(T81, T82, T29, appendB_in_agg(X123, T81, T83))
appendB_in_agg([], T90, T90) → appendB_out_agg([], T90, T90)
appendB_in_agg(.(T98, X148), T97, .(T98, T99)) → U2_agg(T98, X148, T97, T99, appendB_in_agg(X148, T97, T99))
U2_agg(T98, X148, T97, T99, appendB_out_agg(X148, T97, T99)) → appendB_out_agg(.(T98, X148), T97, .(T98, T99))
U6_gg(T81, T82, T29, appendB_out_agg(X123, T81, T83)) → sublistC_out_gg(T81, .(T82, T29))
SUBLISTC_IN_GG(T5, .(T28, T29)) → U3_GG(T5, T28, T29, appendA_in_aag(X56, X57, T29))
SUBLISTC_IN_GG(T5, .(T28, T29)) → APPENDA_IN_AAG(X56, X57, T29)
APPENDA_IN_AAG(.(T49, X93), X94, .(T49, T50)) → U1_AAG(T49, X93, X94, T50, appendA_in_aag(X93, X94, T50))
APPENDA_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPENDA_IN_AAG(X93, X94, T50)
SUBLISTC_IN_GG(.(T71, T72), .(T71, T29)) → U4_GG(T71, T72, T29, appendA_in_gag(T72, T38, T29))
SUBLISTC_IN_GG(.(T71, T72), .(T71, T29)) → APPENDA_IN_GAG(T72, T38, T29)
APPENDA_IN_GAG(.(T49, X93), X94, .(T49, T50)) → U1_GAG(T49, X93, X94, T50, appendA_in_gag(X93, X94, T50))
APPENDA_IN_GAG(.(T49, X93), X94, .(T49, T50)) → APPENDA_IN_GAG(X93, X94, T50)
SUBLISTC_IN_GG(T81, .(T82, T29)) → U5_GG(T81, T82, T29, appendA_in_aag(T83, T38, T29))
U5_GG(T81, T82, T29, appendA_out_aag(T83, T38, T29)) → U6_GG(T81, T82, T29, appendB_in_agg(X123, T81, T83))
U5_GG(T81, T82, T29, appendA_out_aag(T83, T38, T29)) → APPENDB_IN_AGG(X123, T81, T83)
APPENDB_IN_AGG(.(T98, X148), T97, .(T98, T99)) → U2_AGG(T98, X148, T97, T99, appendB_in_agg(X148, T97, T99))
APPENDB_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPENDB_IN_AGG(X148, T97, T99)
sublistC_in_gg([], T15) → sublistC_out_gg([], T15)
sublistC_in_gg(T5, .(T28, T29)) → U3_gg(T5, T28, T29, appendA_in_aag(X56, X57, T29))
appendA_in_aag([], T44, T44) → appendA_out_aag([], T44, T44)
appendA_in_aag(.(T49, X93), X94, .(T49, T50)) → U1_aag(T49, X93, X94, T50, appendA_in_aag(X93, X94, T50))
U1_aag(T49, X93, X94, T50, appendA_out_aag(X93, X94, T50)) → appendA_out_aag(.(T49, X93), X94, .(T49, T50))
U3_gg(T5, T28, T29, appendA_out_aag(X56, X57, T29)) → sublistC_out_gg(T5, .(T28, T29))
sublistC_in_gg(.(T71, T72), .(T71, T29)) → U4_gg(T71, T72, T29, appendA_in_gag(T72, T38, T29))
appendA_in_gag([], T44, T44) → appendA_out_gag([], T44, T44)
appendA_in_gag(.(T49, X93), X94, .(T49, T50)) → U1_gag(T49, X93, X94, T50, appendA_in_gag(X93, X94, T50))
U1_gag(T49, X93, X94, T50, appendA_out_gag(X93, X94, T50)) → appendA_out_gag(.(T49, X93), X94, .(T49, T50))
U4_gg(T71, T72, T29, appendA_out_gag(T72, T38, T29)) → sublistC_out_gg(.(T71, T72), .(T71, T29))
sublistC_in_gg(T81, .(T82, T29)) → U5_gg(T81, T82, T29, appendA_in_aag(T83, T38, T29))
U5_gg(T81, T82, T29, appendA_out_aag(T83, T38, T29)) → U6_gg(T81, T82, T29, appendB_in_agg(X123, T81, T83))
appendB_in_agg([], T90, T90) → appendB_out_agg([], T90, T90)
appendB_in_agg(.(T98, X148), T97, .(T98, T99)) → U2_agg(T98, X148, T97, T99, appendB_in_agg(X148, T97, T99))
U2_agg(T98, X148, T97, T99, appendB_out_agg(X148, T97, T99)) → appendB_out_agg(.(T98, X148), T97, .(T98, T99))
U6_gg(T81, T82, T29, appendB_out_agg(X123, T81, T83)) → sublistC_out_gg(T81, .(T82, T29))
APPENDB_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPENDB_IN_AGG(X148, T97, T99)
sublistC_in_gg([], T15) → sublistC_out_gg([], T15)
sublistC_in_gg(T5, .(T28, T29)) → U3_gg(T5, T28, T29, appendA_in_aag(X56, X57, T29))
appendA_in_aag([], T44, T44) → appendA_out_aag([], T44, T44)
appendA_in_aag(.(T49, X93), X94, .(T49, T50)) → U1_aag(T49, X93, X94, T50, appendA_in_aag(X93, X94, T50))
U1_aag(T49, X93, X94, T50, appendA_out_aag(X93, X94, T50)) → appendA_out_aag(.(T49, X93), X94, .(T49, T50))
U3_gg(T5, T28, T29, appendA_out_aag(X56, X57, T29)) → sublistC_out_gg(T5, .(T28, T29))
sublistC_in_gg(.(T71, T72), .(T71, T29)) → U4_gg(T71, T72, T29, appendA_in_gag(T72, T38, T29))
appendA_in_gag([], T44, T44) → appendA_out_gag([], T44, T44)
appendA_in_gag(.(T49, X93), X94, .(T49, T50)) → U1_gag(T49, X93, X94, T50, appendA_in_gag(X93, X94, T50))
U1_gag(T49, X93, X94, T50, appendA_out_gag(X93, X94, T50)) → appendA_out_gag(.(T49, X93), X94, .(T49, T50))
U4_gg(T71, T72, T29, appendA_out_gag(T72, T38, T29)) → sublistC_out_gg(.(T71, T72), .(T71, T29))
sublistC_in_gg(T81, .(T82, T29)) → U5_gg(T81, T82, T29, appendA_in_aag(T83, T38, T29))
U5_gg(T81, T82, T29, appendA_out_aag(T83, T38, T29)) → U6_gg(T81, T82, T29, appendB_in_agg(X123, T81, T83))
appendB_in_agg([], T90, T90) → appendB_out_agg([], T90, T90)
appendB_in_agg(.(T98, X148), T97, .(T98, T99)) → U2_agg(T98, X148, T97, T99, appendB_in_agg(X148, T97, T99))
U2_agg(T98, X148, T97, T99, appendB_out_agg(X148, T97, T99)) → appendB_out_agg(.(T98, X148), T97, .(T98, T99))
U6_gg(T81, T82, T29, appendB_out_agg(X123, T81, T83)) → sublistC_out_gg(T81, .(T82, T29))
APPENDB_IN_AGG(.(T98, X148), T97, .(T98, T99)) → APPENDB_IN_AGG(X148, T97, T99)
APPENDB_IN_AGG(T97, .(T98, T99)) → APPENDB_IN_AGG(T97, T99)
From the DPs we obtained the following set of size-change graphs:
APPENDA_IN_GAG(.(T49, X93), X94, .(T49, T50)) → APPENDA_IN_GAG(X93, X94, T50)
sublistC_in_gg([], T15) → sublistC_out_gg([], T15)
sublistC_in_gg(T5, .(T28, T29)) → U3_gg(T5, T28, T29, appendA_in_aag(X56, X57, T29))
appendA_in_aag([], T44, T44) → appendA_out_aag([], T44, T44)
appendA_in_aag(.(T49, X93), X94, .(T49, T50)) → U1_aag(T49, X93, X94, T50, appendA_in_aag(X93, X94, T50))
U1_aag(T49, X93, X94, T50, appendA_out_aag(X93, X94, T50)) → appendA_out_aag(.(T49, X93), X94, .(T49, T50))
U3_gg(T5, T28, T29, appendA_out_aag(X56, X57, T29)) → sublistC_out_gg(T5, .(T28, T29))
sublistC_in_gg(.(T71, T72), .(T71, T29)) → U4_gg(T71, T72, T29, appendA_in_gag(T72, T38, T29))
appendA_in_gag([], T44, T44) → appendA_out_gag([], T44, T44)
appendA_in_gag(.(T49, X93), X94, .(T49, T50)) → U1_gag(T49, X93, X94, T50, appendA_in_gag(X93, X94, T50))
U1_gag(T49, X93, X94, T50, appendA_out_gag(X93, X94, T50)) → appendA_out_gag(.(T49, X93), X94, .(T49, T50))
U4_gg(T71, T72, T29, appendA_out_gag(T72, T38, T29)) → sublistC_out_gg(.(T71, T72), .(T71, T29))
sublistC_in_gg(T81, .(T82, T29)) → U5_gg(T81, T82, T29, appendA_in_aag(T83, T38, T29))
U5_gg(T81, T82, T29, appendA_out_aag(T83, T38, T29)) → U6_gg(T81, T82, T29, appendB_in_agg(X123, T81, T83))
appendB_in_agg([], T90, T90) → appendB_out_agg([], T90, T90)
appendB_in_agg(.(T98, X148), T97, .(T98, T99)) → U2_agg(T98, X148, T97, T99, appendB_in_agg(X148, T97, T99))
U2_agg(T98, X148, T97, T99, appendB_out_agg(X148, T97, T99)) → appendB_out_agg(.(T98, X148), T97, .(T98, T99))
U6_gg(T81, T82, T29, appendB_out_agg(X123, T81, T83)) → sublistC_out_gg(T81, .(T82, T29))
APPENDA_IN_GAG(.(T49, X93), X94, .(T49, T50)) → APPENDA_IN_GAG(X93, X94, T50)
APPENDA_IN_GAG(.(T49, X93), .(T49, T50)) → APPENDA_IN_GAG(X93, T50)
From the DPs we obtained the following set of size-change graphs:
APPENDA_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPENDA_IN_AAG(X93, X94, T50)
sublistC_in_gg([], T15) → sublistC_out_gg([], T15)
sublistC_in_gg(T5, .(T28, T29)) → U3_gg(T5, T28, T29, appendA_in_aag(X56, X57, T29))
appendA_in_aag([], T44, T44) → appendA_out_aag([], T44, T44)
appendA_in_aag(.(T49, X93), X94, .(T49, T50)) → U1_aag(T49, X93, X94, T50, appendA_in_aag(X93, X94, T50))
U1_aag(T49, X93, X94, T50, appendA_out_aag(X93, X94, T50)) → appendA_out_aag(.(T49, X93), X94, .(T49, T50))
U3_gg(T5, T28, T29, appendA_out_aag(X56, X57, T29)) → sublistC_out_gg(T5, .(T28, T29))
sublistC_in_gg(.(T71, T72), .(T71, T29)) → U4_gg(T71, T72, T29, appendA_in_gag(T72, T38, T29))
appendA_in_gag([], T44, T44) → appendA_out_gag([], T44, T44)
appendA_in_gag(.(T49, X93), X94, .(T49, T50)) → U1_gag(T49, X93, X94, T50, appendA_in_gag(X93, X94, T50))
U1_gag(T49, X93, X94, T50, appendA_out_gag(X93, X94, T50)) → appendA_out_gag(.(T49, X93), X94, .(T49, T50))
U4_gg(T71, T72, T29, appendA_out_gag(T72, T38, T29)) → sublistC_out_gg(.(T71, T72), .(T71, T29))
sublistC_in_gg(T81, .(T82, T29)) → U5_gg(T81, T82, T29, appendA_in_aag(T83, T38, T29))
U5_gg(T81, T82, T29, appendA_out_aag(T83, T38, T29)) → U6_gg(T81, T82, T29, appendB_in_agg(X123, T81, T83))
appendB_in_agg([], T90, T90) → appendB_out_agg([], T90, T90)
appendB_in_agg(.(T98, X148), T97, .(T98, T99)) → U2_agg(T98, X148, T97, T99, appendB_in_agg(X148, T97, T99))
U2_agg(T98, X148, T97, T99, appendB_out_agg(X148, T97, T99)) → appendB_out_agg(.(T98, X148), T97, .(T98, T99))
U6_gg(T81, T82, T29, appendB_out_agg(X123, T81, T83)) → sublistC_out_gg(T81, .(T82, T29))
APPENDA_IN_AAG(.(T49, X93), X94, .(T49, T50)) → APPENDA_IN_AAG(X93, X94, T50)
APPENDA_IN_AAG(.(T49, T50)) → APPENDA_IN_AAG(T50)
From the DPs we obtained the following set of size-change graphs: